package probsym;

import gov.nasa.jpf.symbc.Debug;
import gov.nasa.jpf.symbc.probsym.Analyze;

public class TreeMap3 {

  private transient Entry root = null;

	private transient int size = 0;

	private void incrementSize() { /*modCount++;*/
		size++;
	}

	private void decrementSize() { /*modCount++;*/
		size--;
	}

	//--------------------------------------------------------------------
	void covered(int br) {//SPECIFY
		Analyze.coverage(""+br);
		if (br == 7 || br == 9 ||
			br == 34 || br == 37 || br == 40 ||	
			br == 41 || br == 44 || br == 47 || br == 50 || br == 52)
		System.out.println(br);
	}

	//-------------------------------------------------------------------

	public TreeMap3() {
	}

	public int size() {
		return size;
	}

	public boolean containsKey(int key) {
		return getEntry(key) != null;
	}

	private Entry getEntry(int key) {
		Entry p = root;
		while (p != null) {
			if (key == p.key)
				return p;
			else if (key < p.key)
				p = p.left;
			else
				p = p.right;
		}
		return null;
	}

	public void put(int key) {
		Entry t = root;

		if (t == null) {
			covered(1);
			incrementSize();
			root = new Entry(key, null);
			return;
		}

		while (true) {
			if (key == t.key) {
				covered(2);
				return;
			} else if (key < t.key) {
				if (t.left != null) {
					covered(3);
					t = t.left;
				} else {
					covered(4);
					incrementSize();
					t.left = new Entry(key, t);
					fixAfterInsertion(t.left);
					return;
				}
			} else { // key > t.key
				if (t.right != null) {
					covered(5);
					t = t.right;
				} else {
					covered(6);
					incrementSize();
					t.right = new Entry(key, t);
					fixAfterInsertion(t.right);
					return;
				}
			}
		}
	}

	public void remove(int key) {
		Entry p = getEntry(key);
		if (p == null) {
			return;
		}

		deleteEntry(p);
		return;
	}

	public void print() {
		System.out.println("*******************************************");
		if (root != null)
			root.print(0);
		System.out.println("*******************************************");
	}

	public String toString() {
		String res = "";
		if (root != null)
			res = root.toString();
		return res;
	}

	public String concreteString(int max_level) {
		String res = "";
		if (root != null)
			res = root.concreteString(max_level, 0);
		return res;
	}

	private static final boolean RED = false;

	private static final boolean BLACK = true;

	static class Entry {
		int key;

		Entry left = null;

		Entry right = null;

		Entry parent;

		boolean color = BLACK;

		Entry(int key, Entry parent) {
			this.key = key;
			this.parent = parent;
		}

		Entry(int key, Entry left, Entry right, Entry parent, boolean color) {
			this.key = key;
			this.left = left;
			this.right = right;
			this.parent = parent;
			this.color = color;
		}

		public int getKey() {
			return key;
		}

		public String toString() {
			String res = "{ " + (color == BLACK ? "B" : "R") + " ";
			if (left == null)
				res += "null";
			else
				res += left.toString();
			res += " ";
			if (right == null)
				res += "null";
			else
				res += right.toString();
			res += " }";
			return res;
		}

		public String concreteString(int max_level, int cur_level) {
			String res;
			if (cur_level == max_level) {
				res = "{ subtree }";
				//		System.out.println("Brekekek");
			} else {
				res = "{ " + (color == BLACK ? "B" : "R") + key + " ";
				if (left == null)
					res += "null";
				else
					res += left.concreteString(max_level, cur_level + 1);
				res += " ";
				if (right == null)
					res += "null";
				else
					res += right.concreteString(max_level, cur_level + 1);
				res += " }";
			}

			return res;
		}

		public void print(int k) {
			for (int i = 0; i < k; i++)
				System.out.print(" ");
			System.out.println(key + (color == BLACK ? "(B)" : "(R)"));
			for (int i = 0; i < k; i++)
				System.out.print(" ");
			System.out.println("L:");
			if (left != null)
				left.print(k + 2);

			for (int i = 0; i < k; i++)
				System.out.print(" ");
			System.out.println("R:");
			if (right != null)
				right.print(k + 2);
		}

	}

	private Entry successor(Entry t) {
		if (t == null) {
			covered(7);
			return null;
		} else if (t.right != null) {
			Entry p = t.right;
			while (p.left != null) {
				covered(8);
				p = p.left;
			}
			return p;
		} else {
			Entry p = t.parent;
			Entry ch = t;
			while (p != null && ch == p.right) {
				covered(9);
				ch = p;
				p = p.parent;
			}
			return p;
		}
	}

	private static boolean colorOf(Entry p) {
		return (p == null ? BLACK : p.color);
	}

	private static Entry parentOf(Entry p) {
		return (p == null ? null : p.parent);
	}

	private static void setColor(Entry p, boolean c) {
		if (p != null)
			p.color = c;
	}

	private static Entry leftOf(Entry p) {
		return (p == null) ? null : p.left;
	}

	private static Entry rightOf(Entry p) {
		return (p == null) ? null : p.right;
	}

	/** From CLR **/
	private void rotateLeft(Entry p) {
		Entry r = p.right;
		p.right = r.left;
		if (r.left != null) {
			covered(10);
			r.left.parent = p;
		}
		r.parent = p.parent;
		if (p.parent == null) {
			covered(11);
			root = r;
		} else if (p.parent.left == p) {
			covered(12);
			p.parent.left = r;
		} else {
			covered(13);
			p.parent.right = r;
		}
		r.left = p;
		p.parent = r;
	}

	/** From CLR **/
	private void rotateRight(Entry p) {
		Entry l = p.left;
		p.left = l.right;
		if (l.right != null) {
			covered(14);
			l.right.parent = p;
		}
		l.parent = p.parent;
		if (p.parent == null) {
			covered(15);
			root = l;
		} else if (p.parent.right == p) {
			covered(16);
			p.parent.right = l;
		} else {
			covered(17);
			p.parent.left = l;
		}
		l.right = p;
		p.parent = l;
	}

	/** From CLR **/
	private void fixAfterInsertion(Entry x) {
		x.color = RED;

		while (x != null && x != root && x.parent.color == RED) {
			if (parentOf(x) == leftOf(parentOf(parentOf(x)))) {
				Entry y = rightOf(parentOf(parentOf(x)));
				if (colorOf(y) == RED) {
					covered(18);
					setColor(parentOf(x), BLACK);
					setColor(y, BLACK);
					setColor(parentOf(parentOf(x)), RED);
					x = parentOf(parentOf(x));
				} else {
					if (x == rightOf(parentOf(x))) {
						covered(19);
						x = parentOf(x);
						rotateLeft(x);
					}
					setColor(parentOf(x), BLACK);
					setColor(parentOf(parentOf(x)), RED);
					if (parentOf(parentOf(x)) != null) {
						covered(20);
						rotateRight(parentOf(parentOf(x)));
					}
				}
			} else {
				Entry y = leftOf(parentOf(parentOf(x)));
				if (colorOf(y) == RED) {
					covered(21);
					setColor(parentOf(x), BLACK);
					setColor(y, BLACK);
					setColor(parentOf(parentOf(x)), RED);
					x = parentOf(parentOf(x));
				} else {
					if (x == leftOf(parentOf(x))) {
						covered(22);
						x = parentOf(x);
						rotateRight(x);
					}
					setColor(parentOf(x), BLACK);
					setColor(parentOf(parentOf(x)), RED);
					if (parentOf(parentOf(x)) != null) {
						covered(23);
						rotateLeft(parentOf(parentOf(x)));
					}
				}
			}
		}
		root.color = BLACK;
	}

	private void deleteEntry(Entry p) {
		decrementSize();

		// If strictly internal, first swap position with successor.
		if (p.left != null && p.right != null) {
			covered(24);
			Entry s = successor(p);
			swapPosition(s, p);
		}

		// Start fixup at replacement node, if it exists.
		Entry replacement = (p.left != null ? p.left : p.right);

		if (replacement != null) {
			// Link replacement to parent 
			replacement.parent = p.parent;
			if (p.parent == null) {
				covered(25);
				root = replacement;
			} else if (p == p.parent.left) {
				covered(26);
				p.parent.left = replacement;
			} else {
				covered(27);
				p.parent.right = replacement;
			}

			// Null out links so they are OK to use by fixAfterDeletion.
			p.left = p.right = p.parent = null;

			// Fix replacement
			if (p.color == BLACK) {
				covered(28);
				fixAfterDeletion(replacement);
			} // MISSING else { test case .. not reachable anyway}
		} else if (p.parent == null) { // return if we are the only node.
			covered(29);
			root = null;
		} else { //  No children. Use self as phantom replacement and unlink.
			if (p.color == BLACK) {
				covered(30);
				fixAfterDeletion(p);
			}

			if (p.parent != null) {
				covered(31);
				if (p == p.parent.left) {
					covered(32);
					p.parent.left = null;
				} else if (p == p.parent.right) {
					covered(33);
					p.parent.right = null;
				} // MISSING else {test... not reachable}
				p.parent = null;
			} // MISSING else ...
		}
	}

	/** From CLR **/
	private void fixAfterDeletion(Entry x) {
		while (x != root && colorOf(x) == BLACK) {
			if (x == leftOf(parentOf(x))) {
				Entry sib = rightOf(parentOf(x));

				if (colorOf(sib) == RED) {
					//assert false;
					covered(34);
					setColor(sib, BLACK);
					setColor(parentOf(x), RED);
					rotateLeft(parentOf(x));
					sib = rightOf(parentOf(x));
				}

				if (colorOf(leftOf(sib)) == BLACK
						&& colorOf(rightOf(sib)) == BLACK) {
					covered(35);
					setColor(sib, RED);
					x = parentOf(x);
				} else {
					if (colorOf(rightOf(sib)) == BLACK) {
						covered(36);
						setColor(leftOf(sib), BLACK);
						setColor(sib, RED);
						rotateRight(sib);
						sib = rightOf(parentOf(x));
					}
					setColor(sib, colorOf(parentOf(x)));
					setColor(parentOf(x), BLACK);
					setColor(rightOf(sib), BLACK);
					rotateLeft(parentOf(x));
					x = root;
				}
			} else { // symmetric
				Entry sib = leftOf(parentOf(x));

				if (colorOf(sib) == RED) {
					covered(37);
					setColor(sib, BLACK);
					setColor(parentOf(x), RED);
					rotateRight(parentOf(x));
					sib = leftOf(parentOf(x));
				}

				if (colorOf(rightOf(sib)) == BLACK
						&& colorOf(leftOf(sib)) == BLACK) {
					covered(38);
					setColor(sib, RED);
					x = parentOf(x);
				} else {
					if (colorOf(leftOf(sib)) == BLACK) {
						covered(39);
						setColor(rightOf(sib), BLACK);
						setColor(sib, RED);
						rotateLeft(sib);
						sib = leftOf(parentOf(x));
					}
					setColor(sib, colorOf(parentOf(x)));
					setColor(parentOf(x), BLACK);
					setColor(leftOf(sib), BLACK);
					rotateRight(parentOf(x));
					x = root;
				}
			}
		}

		setColor(x, BLACK);
	}

	/**
	 * Swap the linkages of two nodes in a tree.
	 */
	private void swapPosition(Entry x, Entry y) {
		// Save initial values.
		Entry px = x.parent, lx = x.left, rx = x.right;
		Entry py = y.parent, ly = y.left, ry = y.right;
		boolean xWasLeftChild = px != null && x == px.left;
		boolean yWasLeftChild = py != null && y == py.left;

		//	System.out.println("Swap: "+x.key+" "+y.key);
		// Swap, handling special cases of one being the other's parent.
		if (x == py) { // x was y's parent
			x.parent = y;
			if (yWasLeftChild) {
				covered(40);
				y.left = x;
				y.right = rx;
			} else {
				covered(41);
				y.right = x;
				y.left = lx;
			}
		} else {
			x.parent = py;
			if (py != null) {
				if (yWasLeftChild) {
					covered(42);
					py.left = x;
				} else {
					covered(43);
					py.right = x;
				}
			}
			y.left = lx;
			y.right = rx;
		}

		if (y == px) { // y was x's parent
			y.parent = x;
			if (xWasLeftChild) {
				covered(44);
				x.left = y;
				x.right = ry;
			} else {
				covered(45);
				x.right = y;
				x.left = ly;
			}
		} else {
			y.parent = px;
			if (px != null) {
				if (xWasLeftChild) {
					covered(46);
					px.left = y;
				} else {
					covered(47);
					px.right = y;
				}
			}
			x.left = ly;
			x.right = ry;
		}

		// Fix children's parent pointers
		if (x.left != null) {
			covered(48);
			x.left.parent = x;
		}
		if (x.right != null) {
			covered(49);
			x.right.parent = x;
		}
		if (y.left != null) {
			covered(50);
			y.left.parent = y;
		}
		if (y.right != null) {
			covered(51);
			y.right.parent = y;
		}

		// Swap colors
		boolean c = x.color;
		x.color = y.color;
		y.color = c;

		// Check if root changed
		if (root == x) {
			covered(52);
			root = y;
		} else if (root == y) {
			covered(53);
			root = x;
		}
	}
	
	public static void runTest(int[] options, int limit) {
		TreeMap3 b = new TreeMap3();
		int round = 0;
		while (round < limit) {
			if (options[round] == 1) {
				//System.out.println("Insert v1");
				b.put(options[limit + round]);
			}
			else {
				//System.out.println("Delete v1");
				b.remove(options[limit + round]);
			}				
			round++;
		}
	}
	
	
	public static void runTestDriver(int length) {
		int[] values = new int[length*2];
		int i = 0;
		while (i < 2*length) {
			if (i < length)
				values[i] = Debug.makeSymbolicInteger("c" + i);
			else 
				values[i] = Debug.makeSymbolicInteger("v" + i);
			i++;
		}
	    runTest(values,length);
	}
	
	public static void main(String[] Argv) {		
		runTestDriver(3);
	}

}
